The Sweeney-Robertson-Tocher (SRT) algorithm for division and square root extraction is widely used by microprocessors. This algorithm accesses an entry in a lookup table (LUT) on every clock cycle, to provide a fixed number of result bits within the clock cycle.
As every other hardware or software component in a microprocessor, the specific implementation of the algorithm has to be checked thoroughly to ensure that no error is introduced. In particular it is highly important to check that all entries of the LUT are correct.
For simplicity, the discussion below refers to pairs of numbers for testing the division operation, but it should be understood as covering also single numbers for testing the square root operation.
Simulating the algorithm execution, and in particular checking all relevant entries of the table is a highly challenging task. For full coverage, it is required to run the algorithm with input comprising a set of pairs of numbers such that executing the algorithm on the full set will lead to each reachable entry in the table, and for certain entries at least a predetermined number of times.
In addition, it may be required to identify entries in the table which are unreachable, i.e., there is no pair of numbers that the division of which will, on any cycle, lead to these entries. By identifying and removing these entries, the LUT may be made smaller, thus reducing space consumption and increasing efficiency. In any case, identifying the unreachable entries enables testing for full coverage of the reachable entries.
Several approaches have been tried to prove the correctness of SRT based implementations of division and square root extraction. Some of these approaches ensure coverage, but at very high time and complexity requirements, and with additional simulation efforts, thus making them practically impossible. Moreover, none of these approaches was able to provide a set of inputs that ensures that every reachable entry is indeed reached, and prove that other entries cannot be reached.
There is thus a need for a method and system for identifying unreachable entries in a LUT of the SRT algorithm, ensuring coverage of the reachable entries, and providing enough input for testing that the algorithm reaches every reachable entry.